b:, x, y:Top. null(if b then x else y fi ) ~ if b then null(x) else null(y) fi  

latex

ProofTree

Definitions	Top, Unit, P  Q, P & Q, P  Q, , , b, A, b, x:A. B(x), t  T
Lemmas	assert wf, not wf, bnot wf, bool wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, top wf